T:Type, L, L1:T List. L1  L  (L2:T List. interleaving(T;L1;L2;L)) 

latex

Definitions	t  T, x:A. B(x), interleaving(T;L1;L2;L), x:A. B(x), L1  L2, P  Q, P  Q, P & Q, P  Q, P  Q
Lemmas	interleaving symmetry, cons interleaving, cons sublist cons, sublist nil, nil interleaving, sublist wf, interleaving wf